0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 85 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 24 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 78 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 MRRProof (⇔, 49 ms)
↳29 QDP
↳30 PisEmptyProof (⇔, 0 ms)
↳31 YES
permE_in_ga(nil, nil) → permE_out_ga(nil, nil)
permE_in_ga(cons(T30, T31), cons(T30, T32)) → U4_ga(T30, T31, T32, appendC_in_ga(T31, X23))
appendC_in_ga(T40, T40) → appendC_out_ga(T40, T40)
U4_ga(T30, T31, T32, appendC_out_ga(T31, X23)) → permE_out_ga(cons(T30, T31), cons(T30, T32))
permE_in_ga(cons(T30, T31), cons(T30, T32)) → U5_ga(T30, T31, T32, appendC_in_ga(T31, T34))
U5_ga(T30, T31, T32, appendC_out_ga(T31, T34)) → U6_ga(T30, T31, T32, permE_in_ga(T34, T32))
permE_in_ga(cons(T47, T48), cons(T50, T51)) → U7_ga(T47, T48, T50, T51, splitA_in_gaaa(T48, X56, T50, X57))
splitA_in_gaaa(cons(T80, T81), nil, T80, T81) → splitA_out_gaaa(cons(T80, T81), nil, T80, T81)
splitA_in_gaaa(cons(T88, T89), cons(T88, X83), T91, X84) → U1_gaaa(T88, T89, X83, T91, X84, splitA_in_gaaa(T89, X83, T91, X84))
U1_gaaa(T88, T89, X83, T91, X84, splitA_out_gaaa(T89, X83, T91, X84)) → splitA_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)
U7_ga(T47, T48, T50, T51, splitA_out_gaaa(T48, X56, T50, X57)) → permE_out_ga(cons(T47, T48), cons(T50, T51))
permE_in_ga(cons(T47, T48), cons(T50, T60)) → U8_ga(T47, T48, T50, T60, splitA_in_gaaa(T48, T58, T50, T59))
U8_ga(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U9_ga(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, X23))
appendD_in_ggga(T107, T108, T109, cons(T107, X108)) → U3_ggga(T107, T108, T109, X108, appendB_in_gga(T108, T109, X108))
appendB_in_gga(nil, T116, T116) → appendB_out_gga(nil, T116, T116)
appendB_in_gga(cons(T123, T124), T125, cons(T123, X130)) → U2_gga(T123, T124, T125, X130, appendB_in_gga(T124, T125, X130))
U2_gga(T123, T124, T125, X130, appendB_out_gga(T124, T125, X130)) → appendB_out_gga(cons(T123, T124), T125, cons(T123, X130))
U3_ggga(T107, T108, T109, X108, appendB_out_gga(T108, T109, X108)) → appendD_out_ggga(T107, T108, T109, cons(T107, X108))
U9_ga(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, X23)) → permE_out_ga(cons(T47, T48), cons(T50, T60))
U8_ga(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U10_ga(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, T98))
U10_ga(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, T98)) → U11_ga(T47, T48, T50, T60, permE_in_ga(T98, T60))
U11_ga(T47, T48, T50, T60, permE_out_ga(T98, T60)) → permE_out_ga(cons(T47, T48), cons(T50, T60))
U6_ga(T30, T31, T32, permE_out_ga(T34, T32)) → permE_out_ga(cons(T30, T31), cons(T30, T32))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
permE_in_ga(nil, nil) → permE_out_ga(nil, nil)
permE_in_ga(cons(T30, T31), cons(T30, T32)) → U4_ga(T30, T31, T32, appendC_in_ga(T31, X23))
appendC_in_ga(T40, T40) → appendC_out_ga(T40, T40)
U4_ga(T30, T31, T32, appendC_out_ga(T31, X23)) → permE_out_ga(cons(T30, T31), cons(T30, T32))
permE_in_ga(cons(T30, T31), cons(T30, T32)) → U5_ga(T30, T31, T32, appendC_in_ga(T31, T34))
U5_ga(T30, T31, T32, appendC_out_ga(T31, T34)) → U6_ga(T30, T31, T32, permE_in_ga(T34, T32))
permE_in_ga(cons(T47, T48), cons(T50, T51)) → U7_ga(T47, T48, T50, T51, splitA_in_gaaa(T48, X56, T50, X57))
splitA_in_gaaa(cons(T80, T81), nil, T80, T81) → splitA_out_gaaa(cons(T80, T81), nil, T80, T81)
splitA_in_gaaa(cons(T88, T89), cons(T88, X83), T91, X84) → U1_gaaa(T88, T89, X83, T91, X84, splitA_in_gaaa(T89, X83, T91, X84))
U1_gaaa(T88, T89, X83, T91, X84, splitA_out_gaaa(T89, X83, T91, X84)) → splitA_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)
U7_ga(T47, T48, T50, T51, splitA_out_gaaa(T48, X56, T50, X57)) → permE_out_ga(cons(T47, T48), cons(T50, T51))
permE_in_ga(cons(T47, T48), cons(T50, T60)) → U8_ga(T47, T48, T50, T60, splitA_in_gaaa(T48, T58, T50, T59))
U8_ga(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U9_ga(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, X23))
appendD_in_ggga(T107, T108, T109, cons(T107, X108)) → U3_ggga(T107, T108, T109, X108, appendB_in_gga(T108, T109, X108))
appendB_in_gga(nil, T116, T116) → appendB_out_gga(nil, T116, T116)
appendB_in_gga(cons(T123, T124), T125, cons(T123, X130)) → U2_gga(T123, T124, T125, X130, appendB_in_gga(T124, T125, X130))
U2_gga(T123, T124, T125, X130, appendB_out_gga(T124, T125, X130)) → appendB_out_gga(cons(T123, T124), T125, cons(T123, X130))
U3_ggga(T107, T108, T109, X108, appendB_out_gga(T108, T109, X108)) → appendD_out_ggga(T107, T108, T109, cons(T107, X108))
U9_ga(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, X23)) → permE_out_ga(cons(T47, T48), cons(T50, T60))
U8_ga(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U10_ga(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, T98))
U10_ga(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, T98)) → U11_ga(T47, T48, T50, T60, permE_in_ga(T98, T60))
U11_ga(T47, T48, T50, T60, permE_out_ga(T98, T60)) → permE_out_ga(cons(T47, T48), cons(T50, T60))
U6_ga(T30, T31, T32, permE_out_ga(T34, T32)) → permE_out_ga(cons(T30, T31), cons(T30, T32))
PERME_IN_GA(cons(T30, T31), cons(T30, T32)) → U4_GA(T30, T31, T32, appendC_in_ga(T31, X23))
PERME_IN_GA(cons(T30, T31), cons(T30, T32)) → APPENDC_IN_GA(T31, X23)
PERME_IN_GA(cons(T30, T31), cons(T30, T32)) → U5_GA(T30, T31, T32, appendC_in_ga(T31, T34))
U5_GA(T30, T31, T32, appendC_out_ga(T31, T34)) → U6_GA(T30, T31, T32, permE_in_ga(T34, T32))
U5_GA(T30, T31, T32, appendC_out_ga(T31, T34)) → PERME_IN_GA(T34, T32)
PERME_IN_GA(cons(T47, T48), cons(T50, T51)) → U7_GA(T47, T48, T50, T51, splitA_in_gaaa(T48, X56, T50, X57))
PERME_IN_GA(cons(T47, T48), cons(T50, T51)) → SPLITA_IN_GAAA(T48, X56, T50, X57)
SPLITA_IN_GAAA(cons(T88, T89), cons(T88, X83), T91, X84) → U1_GAAA(T88, T89, X83, T91, X84, splitA_in_gaaa(T89, X83, T91, X84))
SPLITA_IN_GAAA(cons(T88, T89), cons(T88, X83), T91, X84) → SPLITA_IN_GAAA(T89, X83, T91, X84)
PERME_IN_GA(cons(T47, T48), cons(T50, T60)) → U8_GA(T47, T48, T50, T60, splitA_in_gaaa(T48, T58, T50, T59))
U8_GA(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U9_GA(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, X23))
U8_GA(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → APPENDD_IN_GGGA(T47, T58, T59, X23)
APPENDD_IN_GGGA(T107, T108, T109, cons(T107, X108)) → U3_GGGA(T107, T108, T109, X108, appendB_in_gga(T108, T109, X108))
APPENDD_IN_GGGA(T107, T108, T109, cons(T107, X108)) → APPENDB_IN_GGA(T108, T109, X108)
APPENDB_IN_GGA(cons(T123, T124), T125, cons(T123, X130)) → U2_GGA(T123, T124, T125, X130, appendB_in_gga(T124, T125, X130))
APPENDB_IN_GGA(cons(T123, T124), T125, cons(T123, X130)) → APPENDB_IN_GGA(T124, T125, X130)
U8_GA(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U10_GA(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, T98))
U10_GA(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, T98)) → U11_GA(T47, T48, T50, T60, permE_in_ga(T98, T60))
U10_GA(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, T98)) → PERME_IN_GA(T98, T60)
permE_in_ga(nil, nil) → permE_out_ga(nil, nil)
permE_in_ga(cons(T30, T31), cons(T30, T32)) → U4_ga(T30, T31, T32, appendC_in_ga(T31, X23))
appendC_in_ga(T40, T40) → appendC_out_ga(T40, T40)
U4_ga(T30, T31, T32, appendC_out_ga(T31, X23)) → permE_out_ga(cons(T30, T31), cons(T30, T32))
permE_in_ga(cons(T30, T31), cons(T30, T32)) → U5_ga(T30, T31, T32, appendC_in_ga(T31, T34))
U5_ga(T30, T31, T32, appendC_out_ga(T31, T34)) → U6_ga(T30, T31, T32, permE_in_ga(T34, T32))
permE_in_ga(cons(T47, T48), cons(T50, T51)) → U7_ga(T47, T48, T50, T51, splitA_in_gaaa(T48, X56, T50, X57))
splitA_in_gaaa(cons(T80, T81), nil, T80, T81) → splitA_out_gaaa(cons(T80, T81), nil, T80, T81)
splitA_in_gaaa(cons(T88, T89), cons(T88, X83), T91, X84) → U1_gaaa(T88, T89, X83, T91, X84, splitA_in_gaaa(T89, X83, T91, X84))
U1_gaaa(T88, T89, X83, T91, X84, splitA_out_gaaa(T89, X83, T91, X84)) → splitA_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)
U7_ga(T47, T48, T50, T51, splitA_out_gaaa(T48, X56, T50, X57)) → permE_out_ga(cons(T47, T48), cons(T50, T51))
permE_in_ga(cons(T47, T48), cons(T50, T60)) → U8_ga(T47, T48, T50, T60, splitA_in_gaaa(T48, T58, T50, T59))
U8_ga(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U9_ga(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, X23))
appendD_in_ggga(T107, T108, T109, cons(T107, X108)) → U3_ggga(T107, T108, T109, X108, appendB_in_gga(T108, T109, X108))
appendB_in_gga(nil, T116, T116) → appendB_out_gga(nil, T116, T116)
appendB_in_gga(cons(T123, T124), T125, cons(T123, X130)) → U2_gga(T123, T124, T125, X130, appendB_in_gga(T124, T125, X130))
U2_gga(T123, T124, T125, X130, appendB_out_gga(T124, T125, X130)) → appendB_out_gga(cons(T123, T124), T125, cons(T123, X130))
U3_ggga(T107, T108, T109, X108, appendB_out_gga(T108, T109, X108)) → appendD_out_ggga(T107, T108, T109, cons(T107, X108))
U9_ga(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, X23)) → permE_out_ga(cons(T47, T48), cons(T50, T60))
U8_ga(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U10_ga(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, T98))
U10_ga(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, T98)) → U11_ga(T47, T48, T50, T60, permE_in_ga(T98, T60))
U11_ga(T47, T48, T50, T60, permE_out_ga(T98, T60)) → permE_out_ga(cons(T47, T48), cons(T50, T60))
U6_ga(T30, T31, T32, permE_out_ga(T34, T32)) → permE_out_ga(cons(T30, T31), cons(T30, T32))
PERME_IN_GA(cons(T30, T31), cons(T30, T32)) → U4_GA(T30, T31, T32, appendC_in_ga(T31, X23))
PERME_IN_GA(cons(T30, T31), cons(T30, T32)) → APPENDC_IN_GA(T31, X23)
PERME_IN_GA(cons(T30, T31), cons(T30, T32)) → U5_GA(T30, T31, T32, appendC_in_ga(T31, T34))
U5_GA(T30, T31, T32, appendC_out_ga(T31, T34)) → U6_GA(T30, T31, T32, permE_in_ga(T34, T32))
U5_GA(T30, T31, T32, appendC_out_ga(T31, T34)) → PERME_IN_GA(T34, T32)
PERME_IN_GA(cons(T47, T48), cons(T50, T51)) → U7_GA(T47, T48, T50, T51, splitA_in_gaaa(T48, X56, T50, X57))
PERME_IN_GA(cons(T47, T48), cons(T50, T51)) → SPLITA_IN_GAAA(T48, X56, T50, X57)
SPLITA_IN_GAAA(cons(T88, T89), cons(T88, X83), T91, X84) → U1_GAAA(T88, T89, X83, T91, X84, splitA_in_gaaa(T89, X83, T91, X84))
SPLITA_IN_GAAA(cons(T88, T89), cons(T88, X83), T91, X84) → SPLITA_IN_GAAA(T89, X83, T91, X84)
PERME_IN_GA(cons(T47, T48), cons(T50, T60)) → U8_GA(T47, T48, T50, T60, splitA_in_gaaa(T48, T58, T50, T59))
U8_GA(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U9_GA(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, X23))
U8_GA(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → APPENDD_IN_GGGA(T47, T58, T59, X23)
APPENDD_IN_GGGA(T107, T108, T109, cons(T107, X108)) → U3_GGGA(T107, T108, T109, X108, appendB_in_gga(T108, T109, X108))
APPENDD_IN_GGGA(T107, T108, T109, cons(T107, X108)) → APPENDB_IN_GGA(T108, T109, X108)
APPENDB_IN_GGA(cons(T123, T124), T125, cons(T123, X130)) → U2_GGA(T123, T124, T125, X130, appendB_in_gga(T124, T125, X130))
APPENDB_IN_GGA(cons(T123, T124), T125, cons(T123, X130)) → APPENDB_IN_GGA(T124, T125, X130)
U8_GA(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U10_GA(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, T98))
U10_GA(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, T98)) → U11_GA(T47, T48, T50, T60, permE_in_ga(T98, T60))
U10_GA(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, T98)) → PERME_IN_GA(T98, T60)
permE_in_ga(nil, nil) → permE_out_ga(nil, nil)
permE_in_ga(cons(T30, T31), cons(T30, T32)) → U4_ga(T30, T31, T32, appendC_in_ga(T31, X23))
appendC_in_ga(T40, T40) → appendC_out_ga(T40, T40)
U4_ga(T30, T31, T32, appendC_out_ga(T31, X23)) → permE_out_ga(cons(T30, T31), cons(T30, T32))
permE_in_ga(cons(T30, T31), cons(T30, T32)) → U5_ga(T30, T31, T32, appendC_in_ga(T31, T34))
U5_ga(T30, T31, T32, appendC_out_ga(T31, T34)) → U6_ga(T30, T31, T32, permE_in_ga(T34, T32))
permE_in_ga(cons(T47, T48), cons(T50, T51)) → U7_ga(T47, T48, T50, T51, splitA_in_gaaa(T48, X56, T50, X57))
splitA_in_gaaa(cons(T80, T81), nil, T80, T81) → splitA_out_gaaa(cons(T80, T81), nil, T80, T81)
splitA_in_gaaa(cons(T88, T89), cons(T88, X83), T91, X84) → U1_gaaa(T88, T89, X83, T91, X84, splitA_in_gaaa(T89, X83, T91, X84))
U1_gaaa(T88, T89, X83, T91, X84, splitA_out_gaaa(T89, X83, T91, X84)) → splitA_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)
U7_ga(T47, T48, T50, T51, splitA_out_gaaa(T48, X56, T50, X57)) → permE_out_ga(cons(T47, T48), cons(T50, T51))
permE_in_ga(cons(T47, T48), cons(T50, T60)) → U8_ga(T47, T48, T50, T60, splitA_in_gaaa(T48, T58, T50, T59))
U8_ga(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U9_ga(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, X23))
appendD_in_ggga(T107, T108, T109, cons(T107, X108)) → U3_ggga(T107, T108, T109, X108, appendB_in_gga(T108, T109, X108))
appendB_in_gga(nil, T116, T116) → appendB_out_gga(nil, T116, T116)
appendB_in_gga(cons(T123, T124), T125, cons(T123, X130)) → U2_gga(T123, T124, T125, X130, appendB_in_gga(T124, T125, X130))
U2_gga(T123, T124, T125, X130, appendB_out_gga(T124, T125, X130)) → appendB_out_gga(cons(T123, T124), T125, cons(T123, X130))
U3_ggga(T107, T108, T109, X108, appendB_out_gga(T108, T109, X108)) → appendD_out_ggga(T107, T108, T109, cons(T107, X108))
U9_ga(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, X23)) → permE_out_ga(cons(T47, T48), cons(T50, T60))
U8_ga(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U10_ga(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, T98))
U10_ga(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, T98)) → U11_ga(T47, T48, T50, T60, permE_in_ga(T98, T60))
U11_ga(T47, T48, T50, T60, permE_out_ga(T98, T60)) → permE_out_ga(cons(T47, T48), cons(T50, T60))
U6_ga(T30, T31, T32, permE_out_ga(T34, T32)) → permE_out_ga(cons(T30, T31), cons(T30, T32))
APPENDB_IN_GGA(cons(T123, T124), T125, cons(T123, X130)) → APPENDB_IN_GGA(T124, T125, X130)
permE_in_ga(nil, nil) → permE_out_ga(nil, nil)
permE_in_ga(cons(T30, T31), cons(T30, T32)) → U4_ga(T30, T31, T32, appendC_in_ga(T31, X23))
appendC_in_ga(T40, T40) → appendC_out_ga(T40, T40)
U4_ga(T30, T31, T32, appendC_out_ga(T31, X23)) → permE_out_ga(cons(T30, T31), cons(T30, T32))
permE_in_ga(cons(T30, T31), cons(T30, T32)) → U5_ga(T30, T31, T32, appendC_in_ga(T31, T34))
U5_ga(T30, T31, T32, appendC_out_ga(T31, T34)) → U6_ga(T30, T31, T32, permE_in_ga(T34, T32))
permE_in_ga(cons(T47, T48), cons(T50, T51)) → U7_ga(T47, T48, T50, T51, splitA_in_gaaa(T48, X56, T50, X57))
splitA_in_gaaa(cons(T80, T81), nil, T80, T81) → splitA_out_gaaa(cons(T80, T81), nil, T80, T81)
splitA_in_gaaa(cons(T88, T89), cons(T88, X83), T91, X84) → U1_gaaa(T88, T89, X83, T91, X84, splitA_in_gaaa(T89, X83, T91, X84))
U1_gaaa(T88, T89, X83, T91, X84, splitA_out_gaaa(T89, X83, T91, X84)) → splitA_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)
U7_ga(T47, T48, T50, T51, splitA_out_gaaa(T48, X56, T50, X57)) → permE_out_ga(cons(T47, T48), cons(T50, T51))
permE_in_ga(cons(T47, T48), cons(T50, T60)) → U8_ga(T47, T48, T50, T60, splitA_in_gaaa(T48, T58, T50, T59))
U8_ga(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U9_ga(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, X23))
appendD_in_ggga(T107, T108, T109, cons(T107, X108)) → U3_ggga(T107, T108, T109, X108, appendB_in_gga(T108, T109, X108))
appendB_in_gga(nil, T116, T116) → appendB_out_gga(nil, T116, T116)
appendB_in_gga(cons(T123, T124), T125, cons(T123, X130)) → U2_gga(T123, T124, T125, X130, appendB_in_gga(T124, T125, X130))
U2_gga(T123, T124, T125, X130, appendB_out_gga(T124, T125, X130)) → appendB_out_gga(cons(T123, T124), T125, cons(T123, X130))
U3_ggga(T107, T108, T109, X108, appendB_out_gga(T108, T109, X108)) → appendD_out_ggga(T107, T108, T109, cons(T107, X108))
U9_ga(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, X23)) → permE_out_ga(cons(T47, T48), cons(T50, T60))
U8_ga(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U10_ga(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, T98))
U10_ga(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, T98)) → U11_ga(T47, T48, T50, T60, permE_in_ga(T98, T60))
U11_ga(T47, T48, T50, T60, permE_out_ga(T98, T60)) → permE_out_ga(cons(T47, T48), cons(T50, T60))
U6_ga(T30, T31, T32, permE_out_ga(T34, T32)) → permE_out_ga(cons(T30, T31), cons(T30, T32))
APPENDB_IN_GGA(cons(T123, T124), T125, cons(T123, X130)) → APPENDB_IN_GGA(T124, T125, X130)
APPENDB_IN_GGA(cons(T123, T124), T125) → APPENDB_IN_GGA(T124, T125)
From the DPs we obtained the following set of size-change graphs:
SPLITA_IN_GAAA(cons(T88, T89), cons(T88, X83), T91, X84) → SPLITA_IN_GAAA(T89, X83, T91, X84)
permE_in_ga(nil, nil) → permE_out_ga(nil, nil)
permE_in_ga(cons(T30, T31), cons(T30, T32)) → U4_ga(T30, T31, T32, appendC_in_ga(T31, X23))
appendC_in_ga(T40, T40) → appendC_out_ga(T40, T40)
U4_ga(T30, T31, T32, appendC_out_ga(T31, X23)) → permE_out_ga(cons(T30, T31), cons(T30, T32))
permE_in_ga(cons(T30, T31), cons(T30, T32)) → U5_ga(T30, T31, T32, appendC_in_ga(T31, T34))
U5_ga(T30, T31, T32, appendC_out_ga(T31, T34)) → U6_ga(T30, T31, T32, permE_in_ga(T34, T32))
permE_in_ga(cons(T47, T48), cons(T50, T51)) → U7_ga(T47, T48, T50, T51, splitA_in_gaaa(T48, X56, T50, X57))
splitA_in_gaaa(cons(T80, T81), nil, T80, T81) → splitA_out_gaaa(cons(T80, T81), nil, T80, T81)
splitA_in_gaaa(cons(T88, T89), cons(T88, X83), T91, X84) → U1_gaaa(T88, T89, X83, T91, X84, splitA_in_gaaa(T89, X83, T91, X84))
U1_gaaa(T88, T89, X83, T91, X84, splitA_out_gaaa(T89, X83, T91, X84)) → splitA_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)
U7_ga(T47, T48, T50, T51, splitA_out_gaaa(T48, X56, T50, X57)) → permE_out_ga(cons(T47, T48), cons(T50, T51))
permE_in_ga(cons(T47, T48), cons(T50, T60)) → U8_ga(T47, T48, T50, T60, splitA_in_gaaa(T48, T58, T50, T59))
U8_ga(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U9_ga(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, X23))
appendD_in_ggga(T107, T108, T109, cons(T107, X108)) → U3_ggga(T107, T108, T109, X108, appendB_in_gga(T108, T109, X108))
appendB_in_gga(nil, T116, T116) → appendB_out_gga(nil, T116, T116)
appendB_in_gga(cons(T123, T124), T125, cons(T123, X130)) → U2_gga(T123, T124, T125, X130, appendB_in_gga(T124, T125, X130))
U2_gga(T123, T124, T125, X130, appendB_out_gga(T124, T125, X130)) → appendB_out_gga(cons(T123, T124), T125, cons(T123, X130))
U3_ggga(T107, T108, T109, X108, appendB_out_gga(T108, T109, X108)) → appendD_out_ggga(T107, T108, T109, cons(T107, X108))
U9_ga(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, X23)) → permE_out_ga(cons(T47, T48), cons(T50, T60))
U8_ga(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U10_ga(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, T98))
U10_ga(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, T98)) → U11_ga(T47, T48, T50, T60, permE_in_ga(T98, T60))
U11_ga(T47, T48, T50, T60, permE_out_ga(T98, T60)) → permE_out_ga(cons(T47, T48), cons(T50, T60))
U6_ga(T30, T31, T32, permE_out_ga(T34, T32)) → permE_out_ga(cons(T30, T31), cons(T30, T32))
SPLITA_IN_GAAA(cons(T88, T89), cons(T88, X83), T91, X84) → SPLITA_IN_GAAA(T89, X83, T91, X84)
SPLITA_IN_GAAA(cons(T88, T89)) → SPLITA_IN_GAAA(T89)
From the DPs we obtained the following set of size-change graphs:
PERME_IN_GA(cons(T30, T31), cons(T30, T32)) → U5_GA(T30, T31, T32, appendC_in_ga(T31, T34))
U5_GA(T30, T31, T32, appendC_out_ga(T31, T34)) → PERME_IN_GA(T34, T32)
PERME_IN_GA(cons(T47, T48), cons(T50, T60)) → U8_GA(T47, T48, T50, T60, splitA_in_gaaa(T48, T58, T50, T59))
U8_GA(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U10_GA(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, T98))
U10_GA(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, T98)) → PERME_IN_GA(T98, T60)
permE_in_ga(nil, nil) → permE_out_ga(nil, nil)
permE_in_ga(cons(T30, T31), cons(T30, T32)) → U4_ga(T30, T31, T32, appendC_in_ga(T31, X23))
appendC_in_ga(T40, T40) → appendC_out_ga(T40, T40)
U4_ga(T30, T31, T32, appendC_out_ga(T31, X23)) → permE_out_ga(cons(T30, T31), cons(T30, T32))
permE_in_ga(cons(T30, T31), cons(T30, T32)) → U5_ga(T30, T31, T32, appendC_in_ga(T31, T34))
U5_ga(T30, T31, T32, appendC_out_ga(T31, T34)) → U6_ga(T30, T31, T32, permE_in_ga(T34, T32))
permE_in_ga(cons(T47, T48), cons(T50, T51)) → U7_ga(T47, T48, T50, T51, splitA_in_gaaa(T48, X56, T50, X57))
splitA_in_gaaa(cons(T80, T81), nil, T80, T81) → splitA_out_gaaa(cons(T80, T81), nil, T80, T81)
splitA_in_gaaa(cons(T88, T89), cons(T88, X83), T91, X84) → U1_gaaa(T88, T89, X83, T91, X84, splitA_in_gaaa(T89, X83, T91, X84))
U1_gaaa(T88, T89, X83, T91, X84, splitA_out_gaaa(T89, X83, T91, X84)) → splitA_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)
U7_ga(T47, T48, T50, T51, splitA_out_gaaa(T48, X56, T50, X57)) → permE_out_ga(cons(T47, T48), cons(T50, T51))
permE_in_ga(cons(T47, T48), cons(T50, T60)) → U8_ga(T47, T48, T50, T60, splitA_in_gaaa(T48, T58, T50, T59))
U8_ga(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U9_ga(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, X23))
appendD_in_ggga(T107, T108, T109, cons(T107, X108)) → U3_ggga(T107, T108, T109, X108, appendB_in_gga(T108, T109, X108))
appendB_in_gga(nil, T116, T116) → appendB_out_gga(nil, T116, T116)
appendB_in_gga(cons(T123, T124), T125, cons(T123, X130)) → U2_gga(T123, T124, T125, X130, appendB_in_gga(T124, T125, X130))
U2_gga(T123, T124, T125, X130, appendB_out_gga(T124, T125, X130)) → appendB_out_gga(cons(T123, T124), T125, cons(T123, X130))
U3_ggga(T107, T108, T109, X108, appendB_out_gga(T108, T109, X108)) → appendD_out_ggga(T107, T108, T109, cons(T107, X108))
U9_ga(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, X23)) → permE_out_ga(cons(T47, T48), cons(T50, T60))
U8_ga(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U10_ga(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, T98))
U10_ga(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, T98)) → U11_ga(T47, T48, T50, T60, permE_in_ga(T98, T60))
U11_ga(T47, T48, T50, T60, permE_out_ga(T98, T60)) → permE_out_ga(cons(T47, T48), cons(T50, T60))
U6_ga(T30, T31, T32, permE_out_ga(T34, T32)) → permE_out_ga(cons(T30, T31), cons(T30, T32))
PERME_IN_GA(cons(T30, T31), cons(T30, T32)) → U5_GA(T30, T31, T32, appendC_in_ga(T31, T34))
U5_GA(T30, T31, T32, appendC_out_ga(T31, T34)) → PERME_IN_GA(T34, T32)
PERME_IN_GA(cons(T47, T48), cons(T50, T60)) → U8_GA(T47, T48, T50, T60, splitA_in_gaaa(T48, T58, T50, T59))
U8_GA(T47, T48, T50, T60, splitA_out_gaaa(T48, T58, T50, T59)) → U10_GA(T47, T48, T50, T60, appendD_in_ggga(T47, T58, T59, T98))
U10_GA(T47, T48, T50, T60, appendD_out_ggga(T47, T58, T59, T98)) → PERME_IN_GA(T98, T60)
appendC_in_ga(T40, T40) → appendC_out_ga(T40, T40)
splitA_in_gaaa(cons(T80, T81), nil, T80, T81) → splitA_out_gaaa(cons(T80, T81), nil, T80, T81)
splitA_in_gaaa(cons(T88, T89), cons(T88, X83), T91, X84) → U1_gaaa(T88, T89, X83, T91, X84, splitA_in_gaaa(T89, X83, T91, X84))
appendD_in_ggga(T107, T108, T109, cons(T107, X108)) → U3_ggga(T107, T108, T109, X108, appendB_in_gga(T108, T109, X108))
U1_gaaa(T88, T89, X83, T91, X84, splitA_out_gaaa(T89, X83, T91, X84)) → splitA_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)
U3_ggga(T107, T108, T109, X108, appendB_out_gga(T108, T109, X108)) → appendD_out_ggga(T107, T108, T109, cons(T107, X108))
appendB_in_gga(nil, T116, T116) → appendB_out_gga(nil, T116, T116)
appendB_in_gga(cons(T123, T124), T125, cons(T123, X130)) → U2_gga(T123, T124, T125, X130, appendB_in_gga(T124, T125, X130))
U2_gga(T123, T124, T125, X130, appendB_out_gga(T124, T125, X130)) → appendB_out_gga(cons(T123, T124), T125, cons(T123, X130))
PERME_IN_GA(cons(T30, T31)) → U5_GA(appendC_in_ga(T31))
U5_GA(appendC_out_ga(T34)) → PERME_IN_GA(T34)
PERME_IN_GA(cons(T47, T48)) → U8_GA(T47, splitA_in_gaaa(T48))
U8_GA(T47, splitA_out_gaaa(T58, T50, T59)) → U10_GA(appendD_in_ggga(T47, T58, T59))
U10_GA(appendD_out_ggga(T98)) → PERME_IN_GA(T98)
appendC_in_ga(T40) → appendC_out_ga(T40)
splitA_in_gaaa(cons(T80, T81)) → splitA_out_gaaa(nil, T80, T81)
splitA_in_gaaa(cons(T88, T89)) → U1_gaaa(T88, splitA_in_gaaa(T89))
appendD_in_ggga(T107, T108, T109) → U3_ggga(T107, appendB_in_gga(T108, T109))
U1_gaaa(T88, splitA_out_gaaa(X83, T91, X84)) → splitA_out_gaaa(cons(T88, X83), T91, X84)
U3_ggga(T107, appendB_out_gga(X108)) → appendD_out_ggga(cons(T107, X108))
appendB_in_gga(nil, T116) → appendB_out_gga(T116)
appendB_in_gga(cons(T123, T124), T125) → U2_gga(T123, appendB_in_gga(T124, T125))
U2_gga(T123, appendB_out_gga(X130)) → appendB_out_gga(cons(T123, X130))
appendC_in_ga(x0)
splitA_in_gaaa(x0)
appendD_in_ggga(x0, x1, x2)
U1_gaaa(x0, x1)
U3_ggga(x0, x1)
appendB_in_gga(x0, x1)
U2_gga(x0, x1)
PERME_IN_GA(cons(T30, T31)) → U5_GA(appendC_in_ga(T31))
U5_GA(appendC_out_ga(T34)) → PERME_IN_GA(T34)
PERME_IN_GA(cons(T47, T48)) → U8_GA(T47, splitA_in_gaaa(T48))
U8_GA(T47, splitA_out_gaaa(T58, T50, T59)) → U10_GA(appendD_in_ggga(T47, T58, T59))
U10_GA(appendD_out_ggga(T98)) → PERME_IN_GA(T98)
appendC_in_ga(T40) → appendC_out_ga(T40)
splitA_in_gaaa(cons(T80, T81)) → splitA_out_gaaa(nil, T80, T81)
splitA_in_gaaa(cons(T88, T89)) → U1_gaaa(T88, splitA_in_gaaa(T89))
appendD_in_ggga(T107, T108, T109) → U3_ggga(T107, appendB_in_gga(T108, T109))
U1_gaaa(T88, splitA_out_gaaa(X83, T91, X84)) → splitA_out_gaaa(cons(T88, X83), T91, X84)
U3_ggga(T107, appendB_out_gga(X108)) → appendD_out_ggga(cons(T107, X108))
appendB_in_gga(nil, T116) → appendB_out_gga(T116)
appendB_in_gga(cons(T123, T124), T125) → U2_gga(T123, appendB_in_gga(T124, T125))
U2_gga(T123, appendB_out_gga(X130)) → appendB_out_gga(cons(T123, X130))
U10GA1 > appendDinggga3 > splitAingaaa1 > appendCoutga1 > cons2 > U5GA1 > PERMEINGA1 > U1gaaa2 > U8GA2 > appendBingga2 > U2gga2 > U3ggga2 > appendDoutggga1 > appendBoutgga1 > nil > splitAoutgaaa3 > appendCinga1
nil=4
appendC_in_ga_1=3
appendC_out_ga_1=2
splitA_in_gaaa_1=3
appendB_out_gga_1=4
appendD_out_ggga_1=3
PERME_IN_GA_1=3
U5_GA_1=1
U10_GA_1=1
cons_2=1
splitA_out_gaaa_3=0
U1_gaaa_2=1
appendD_in_ggga_3=0
U3_ggga_2=0
appendB_in_gga_2=0
U2_gga_2=1
U8_GA_2=1
appendC_in_ga(x0)
splitA_in_gaaa(x0)
appendD_in_ggga(x0, x1, x2)
U1_gaaa(x0, x1)
U3_ggga(x0, x1)
appendB_in_gga(x0, x1)
U2_gga(x0, x1)